Theorem ralima 7166

Description: Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) Reduce DV conditions. (Revised by Matthew House, 14-Aug-2025.)

Hypothesis

Ref	Expression
ralima.x	⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralima	⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓))

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝐹,𝑦   𝑥,𝐵,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem ralima

Step	Hyp	Ref	Expression
1		fnfun 6576	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	funfnd 6507	. 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 Fn dom 𝐹)
3		fndm 6579	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	sseq2d 3962	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴))
5	4	biimpar 477	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ dom 𝐹)
6		fvexd 6832	. . 3 ⊢ (((𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹) ∧ 𝑦 ∈ 𝐵) → (𝐹‘𝑦) ∈ V)
7		fvelimab 6889	. . . 4 ⊢ ((𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹) → (𝑥 ∈ (𝐹 “ 𝐵) ↔ ∃𝑦 ∈ 𝐵 (𝐹‘𝑦) = 𝑥))
8		eqcom 2738	. . . . 5 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
9	8	rexbii 3079	. . . 4 ⊢ (∃𝑦 ∈ 𝐵 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐵 𝑥 = (𝐹‘𝑦))
10	7, 9	bitrdi 287	. . 3 ⊢ ((𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹) → (𝑥 ∈ (𝐹 “ 𝐵) ↔ ∃𝑦 ∈ 𝐵 𝑥 = (𝐹‘𝑦)))
11		ralima.x	. . . 4 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
12	11	adantl 481	. . 3 ⊢ (((𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹) ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
13	6, 10, 12	ralxfr2d 5343	. 2 ⊢ ((𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓))
14	2, 5, 13	syl2an2r 685	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056  Vcvv 3436   ⊆ wss 3897  dom cdm 5611   “ cima 5614   Fn wfn 6471  ‘cfv 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-fv 6484

This theorem is referenced by:  rexima  7167  supisolem  9353  ordtypelem6  9404  ordtypelem7  9405  limsupgle  15379  mrcuni  17522  ipodrsima  18442  mgmhmima  18618  mhmimalem  18727  ghmnsgima  19147  cntzmhm  19248  rhmimasubrnglem  20475  qtopeu  23626  kqdisj  23642  ghmcnp  24025  qustgplem  24031  qtopbaslem  24668  bndth  24879  fmcfil  25194  ovoliunlem1  25425  volsup2  25528  mbflimsup  25589  itg2gt0  25683  mdegleb  25991  efopn  26589  fsumdvdsmul  27127  fsumdvdsmulOLD  27129  negsunif  27992  negsbdaylem  27993  onsiso  28200  bdayn0p1  28289  imaelshi  32030  vonf1owev  35144  cvmopnlem  35314  weiunfrlem  36498  ovoliunnfl  37702  voliunnfl  37704  volsupnfl  37705  gicabl  43132  permac8prim  45047