Description: Virtual deduction generalizing rule for one quantifying variable and one
virtual hypothesis without distinct variables. alrimih is gen11nv without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011)(Proof modification is discouraged.)(New usage is discouraged.)