Theorem ralrn 7063

Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)

Hypothesis

Ref	Expression
rexrn.1	⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralrn	⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

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

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

Proof of Theorem ralrn

Step	Hyp	Ref	Expression
1		fvexd 6876	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6924	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2737	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3077	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 287	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5368	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054  Vcvv 3450  ran crn 5642   Fn wfn 6509  ‘cfv 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fn 6517  df-fv 6522

This theorem is referenced by:  ralrnmptw  7069  ralrnmpt  7071  cbvfo  7267  isoselem  7319  indexfi  9318  ordtypelem9  9486  ordtypelem10  9487  wemapwe  9657  numacn  10009  acndom  10011  rpnnen1lem3  12945  fsequb2  13948  limsuple  15451  limsupval2  15453  climsup  15643  ruclem11  16215  ruclem12  16216  prmreclem6  16899  imasaddfnlem  17498  imasvscafn  17507  cycsubgcl  19145  ghmrn  19168  ghmnsgima  19179  pgpssslw  19551  gexex  19790  dprdfcntz  19954  znf1o  21468  frlmlbs  21713  lindfrn  21737  ptcnplem  23515  kqt0lem  23630  isr0  23631  regr1lem2  23634  uzrest  23791  tmdgsum2  23990  imasf1oxmet  24270  imasf1omet  24271  bndth  24864  evth  24865  ovolficcss  25377  ovollb2lem  25396  ovolunlem1  25405  ovoliunlem1  25410  ovoliunlem2  25411  ovoliun2  25414  ovolscalem1  25421  ovolicc1  25424  voliunlem2  25459  voliunlem3  25460  ioombl1lem4  25469  uniioovol  25487  uniioombllem2  25491  uniioombllem3  25493  uniioombllem6  25496  volsup2  25513  vitalilem3  25518  mbfsup  25572  mbfinf  25573  mbflimsup  25574  itg1ge0  25594  itg1mulc  25612  itg1climres  25622  mbfi1fseqlem4  25626  itg2seq  25650  itg2monolem1  25658  itg2mono  25661  itg2i1fseq2  25664  itg2gt0  25668  itg2cnlem1  25669  itg2cn  25671  limciun  25802  plycpn  26204  hmopidmchi  32087  hmopidmpji  32088  rge0scvg  33946  mclsax  35563  mblfinlem2  37659  ismtyhmeolem  37805  nacsfix  42707  fnwe2lem2  43047  gneispace  44130  climinf  45611  liminfval2  45773